  \documentclass{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}
\usepackage{davidemacro}
\usepackage{evolvablemacro}


\usepackage{color}
\newcommand{\emphcolor}[1]{\textcolor{magenta}{#1}\xspace}

\title[Adaptable Processes]{Adaptable Processes}
\author[Cinzia Di Giusto]{M. Bravetti \and \emphcolor{Cinzia Di Giusto} \and J. A. P\'erez \and G. Zavattaro}
\date[]{LMaSI -- CEA}
  
\institute[INRIA Rh\^onealpes]{Universit\`a di Bologna,
INRIA Rh\^{o}ne-Alpes, 
FCT New University of Lisbon}

\setbeamertemplate{navigation symbols}{} 

%\usecolortheme{crane}
%\useoutertheme{progressbar}
%\useinnertheme{progressbar}
%\usefonttheme{progressbar}

\usetheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}
\newcommand{\whitecolor}[1]{\textcolor{white}{#1}\xspace}
\newcommand{\hidecolor}[1]{\textcolor{darkgray}{#1}\xspace}
\newcommand{\olivecolor}[1]{\textcolor{orange}{#1}\xspace}

%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}


%\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
%\newcommand{\til}[1]{\widetilde{#1}}
%\newcommand{\update}[2]{\til{#1}\{#2\} } 
%\newcommand{\component}[2]{#1 [#2]   }  %a[P]
%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output

\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bbl}[1]{\begin{block}{#1}}
\newcommand{\ebl}{\end{block}}

% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}


\begin{document}

\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}


\begin{frame}
 \frametitle{Who am I?}

\begin{block}{ CV}
 \footnotesize
\begin{itemize}
 \item 2010 -- now: {\bf Post doc},  Inria Rh\^{o}ne Alpes, \'equipe Sardes (Advisor: JB Stefani) \\
 \item 2008 -- 2009: {\bf Post doc}, University of Bologna\\
 (Advisor: M. Gabbrielli)\\
 \item  2005 -- 2008: {\bf PhD} in Computer Science\\ (Advisor: M. Gabbrielli)\\
 \end{itemize}
\end{block}
\vspace{0.2cm}
\begin{block}{My research in a sentence}
\centering
Studies of expressiveness and analysis of concurrent calculi (Variants of CCS, Higher order $\pi$, Graph rewriting, \dots)  
\end{block}
\end{frame}

\section{Motivation}
\begin{frame}
 \frametitle{The idea}

\begin{block}{Our aim}
\centering
 We propose a language that  describes the \emphcolor{dynamic} process evolution: i.e. all scenarios where a direct manipulation of the process is required. 
\end{block}

\end{frame}


\begin{frame}
 \frametitle{Motivation}

Concurrency is often associated to dynamic behaviors:

\vspace{0.2cm}

\begin{itemize}
  \item In the $\pi$-calculus, \emphcolor{dynamic network topologies} are obtained through channel/link mobility

    \vspace{0.2cm}
  \item In the Ambient calculus, \emphcolor{dynamic spatial topologies} are obtained through ambient  mobility

\end{itemize}

\end{frame}


\begin{frame}
\frametitle{But \dots}

\begin{itemize}
 \item Neither $\pi$ nor Ambient can describe changes that occur at the process level.
\vspace{0.2cm}
 \item They cannot influence the evolution of the process along time
\end{itemize}

\vspace{0.5cm}
\pause
\begin{block}{}
We need a mechanism so that processes can be 
\begin{itemize}
 \item Stopped
 \item Restarted
 \item Modified 
\end{itemize}
 
\end{block}

 

\end{frame}

\begin{frame}
\frametitle{Inspirations}

As we need a mechanism that handles processes:
\vspace{0.2cm}

\begin{itemize}
 \item we looked  at \emphcolor{higher order} formalisms (Higher Order $\pi$)
\vspace{0.2cm}
 \item we borrowed inspiration (in particular) from the suspension operator of the Kell-calculus
\vspace{0.2cm}
\item In Kell, processes can be suspended and then sent along a channel 

\end{itemize}

 

\end{frame}





\begin{frame}

\frametitle{Our approach}
%A \str{} to the analysis of \str{evolvable systems} 


We are mainly concerned with \emphcolor{dynamic reconfiguration} issues:\\
\vspace{0.2cm}
\begin{itemize}
\item finding proper \emphcolor{evolution/reconfiguration} mechanisms 
\vspace{0.2cm}
\item understanding the \emphcolor{properties} evolvable systems should ensure 
\end{itemize}
 \pause
\begin{block}{Our proposal}
\begin{itemize}
\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} 
\vspace{0.2cm}
\item \emphcolor{Verification problems} for evolvable systems defined in \evol{} 
\vspace{0.2cm}
\item \emphcolor{(Un)decidability results} for such problems
\end{itemize}
\end{block}

 
\end{frame}

\section{Calculi}


\begin{frame}[t]
\frametitle{A calculus for adaptable processes }

\begin{block}{Syntax}
CCS without restriction \only<2->{plus \emphcolor{localities}}\only<3->{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \sum_{i \in I} \pi_i.P_i   \, \mid \, 
          P \parallel P  \, \mid \, ! \pi.P \, \only<2->{\mid \, \emphcolor{\component{a}{P}}}\\ \\
\pi   ::=&  a \, \mid \, \outC{a} \only<3->{\, \mid \, \emphcolorb{\update{a}{U}}}\\ \\
\only<3->{\emphcolorb{U ::=} & \emphcolorb{\sum_{i \in I} \pi_i.U_i  \, \mid \,  \component{a}{U}  \, \mid \, 
          U \parallel U  \, \mid \,  ! \pi.U \, \mid \,  \bullet}}
\end{array}
$$
\only<3->{where 
\begin{itemize}
\item $\component{a}{P}$ is the \emphcolor{adaptable process} $P$ \emphcolor{located at} name $a$
\item $U$ is a \emphcolorb{context}, with zero or more \emphcolorb{holes}, denoted $\bullet$
\end{itemize}}
\end{block}

\end{frame}


\begin{frame}
 \frametitle{Operational Semantic: standard rules}

\begin{block}{Operational Semantics: LTS}

$$
\inferrule[\rulename{Act1}]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}
\quad
\inferrule[\rulename{Tau1}]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
$$
\vspace{0.5cm}
$$
\inferrule[\rulename{Sum}]{}{\sum_{i\in I} \alpha_i.P_i \arro{~\alpha_i~}  P_i } 
\qquad
\inferrule[\textsc{(Repl)}]{}{!\alpha.P \arro{~\alpha~}  P \parallel !\alpha.P }
$$
\end{block}

\end{frame}




\begin{frame}
\frametitle{Operational Semantics: Intuitions}

\begin{block}{Locations}
\begin{itemize}
\item The localities are \emphcolor{transparent}:
$$
 \rightinfer
 			{\component{a}{P} \xrightarrow{~\alpha~}  \component{a}{P'}}
 			{P \xrightarrow{~\alpha~} P'} 
			$$
\end{itemize}			
\end{block}

\pause

\begin{block}{Reconfiguration}
\begin{itemize}

\item Dynamic reconfiguration is obtained  via an interaction  with update prefixes:
$$
\component{a}{P} \parallel \update{a}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$

\item{Process $\fillcon{U}{P}$ is obtained by filling in the holes in $U$ with $P$}
\end{itemize}
\end{block}

\end{frame}

\frame{
\frametitle{Operational Semantics: new rules}

\begin{block}{Operational Semantics: LTS}

%A Labeled Transition System (LTS) which extends that of C
$$
\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\qquad 
\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
$$
\vspace{0.5cm}
$$
\inferrule[\rulename{Tau3}]{P_1 \arro{~\component{a}{\emphcolor{Q}}~} P_1'\andalso P_2 \arro{~\update{a}{\emphcolorb{U}}~} P_2' }{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{\emphcolorb{U}}{\emphcolor{Q}}  }{\star} \parallel P_2'}
$$
\end{block}
}









\frame{
\frametitle{A first example}

A basic client-server scenario:   
\begin{align*}
& \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.C} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
\pired ~ & \componentbbig{client}{\component{run}{P} \parallel  C} \parallel \componentbbig{server}{\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
\pired ~ & \componentbbig{client}{\component{run}{Q \parallel old.P} \parallel C} \parallel \componentbbig{server}{S}
\end{align*}

}

\begin{frame}
\frametitle{Some evolvability patterns}
\begin{itemize}
\item<1->\emphcolorb{Deep update}
 $$\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\component{d}{S_2}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \emphcolor{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\item<2->\emphcolorb{Destroyer}$$ \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (\bullet \not \in Q)$$
\item<3>\emphcolorb{Plug-in} $$\component{a}{Q} \parallel \update{a}{\component{a}{c{.}\bullet +R}}.\nil \pired \component{a}{c{.}Q +\fillcon{R}{Q}} \parallel \nil$$ 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Some evolvability patterns}
\begin{itemize}
\item<1->\emphcolorb{Renaming} $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{\bullet}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item<2->\emphcolorb{Backup} $$\component{a}{Q} \parallel \update{a}{\component{a}{\bullet} \parallel \component{b}{\bullet}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\item<3>\emphcolorb{Replacement} $$ \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$$ 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Static vs Dynamic updates} 

\begin{itemize}
 \item All kinds of update are permitted $ \quad \leadsto \quad$ Dynamic Topology
\vspace{0.2cm} 
 \item Adaptable processes are invariant along the evolution (i.e. they cannot be destroyed nor created)
$$U ::=\sum_{i \in I} \pi_i.U_i  \, \mid \,  \component{a}{U}  \, \mid \, 
          U \parallel U  \, \mid \,  ! \pi.U \, \mid \,  \bullet
$$


\end{itemize}
\pause
\begin{block}{Static topology}
\begin{itemize}
 \item Both syntactic and semantic restriction
\end{itemize}

\end{block}
\end{frame}


\begin{frame}
\frametitle{Static topology}
\begin{enumerate}
 \item Syntax
$$
\begin{array}{lcl}
P       & ::=& \component{a}{P} \, \mid \,
          P \parallel P \, \mid \, \emphcolor{A} \\ %! \pi.A \sepr \sum_{i \in I} \pi_i.A_i  \\
A       & ::=&  \emphcolor{A \parallel A \, \mid \,
          ! \pi.A \, \mid \, \sum_{i \in I} \pi_i.A_i} \qquad
\pi  ::=  a \, \mid \, \outC{a} \, \mid \, \emphcolor{\update{a}{\component{a}{U} \parallel A}}
\end{array}
$$ 
\pause
\item Semantics
$$
\inferrule{P_1 \arro{~\component{a}{Q}~} P_1'\andalso P_2 \arro{~\update{a}{U}~} P_2'  \andalso \mathsf{cond}(U,Q)}{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{U}{Q}  }{\star} \parallel P_2'}
$$
where  $\mathsf{cond}(U,Q)$ holds if\\
\vspace{0.1cm}
%  \begin{enumerate}
  -- $U=\component{a}{U'}\parallel A$ and $\CStr(\component{a}{Q}) = \CStr(\component{a}{\fillcon{U'}{Q}} \parallel A)$\\
\vspace{0.1cm}
  -- if $\numph{U} > 0$ then  $\numap{Q} = 0$.
 % \end{enumerate}



\end{enumerate}
 
\end{frame}

\begin{frame}
 \frametitle{Remarks on Static topology}

\begin{itemize}
 \item Syntactic and semantics restrictions are needed to  be as permissive as possible
\end{itemize}

\vspace{0.5cm}

\begin{theorem}\label{stdynequiv}
Let $P$  be an \evols{} process.
 Then we have:
$$P \pired_s P'\text{ if and only if }\llbracket P\rrbracket  \pired_d \llbracket P'\rrbracket $$
\end{theorem}
\end{frame}









\section{Properties}





\begin{frame}
\frametitle{Verification problems for adaptable processes}

An evolvable system is composed of:
\vspace{0.2cm}
\begin{itemize}
 \item an \emphcolor{initial configuration} $P$ 
\vspace{0.2cm}
 \item an arbitrary number of \emphcolorb{reconfigurations} $\mathcal{M}$
\end{itemize}
 \vspace{0.5cm}

\pause
\begin{itemize}
 \item We observe the system's behavior using \emphcolor{barbs}. 
\vspace{0.2cm}
 \item These observables represent \emphcolor{special signals}: errors, interrupts.

\end{itemize}



\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario}
\only<1>{\includegraphics[height=50mm]{cluster0.pdf}}
\only<2>{\includegraphics[height=50mm]{cluster2.pdf}}
\only<3>{\includegraphics[height=50mm]{cluster1.pdf}}
\only<4>{\includegraphics[height=50mm]{cluster3.pdf}}
\only<5>{\includegraphics[height=50mm]{cluster4.pdf}}
\end{frame}








\begin{frame}
\frametitle{Verification problems for adaptable processes}
Given:
\begin{itemize}
 \item an initial configuration $P$, 
 \item a set of reconfigurations,
 \item a special error signal $e$.
\end{itemize}

\vspace{0.2cm}
\begin{block}{}
\centering 
We would like to know if  for every reachable configuration exposing $e$ the system:

\begin{enumerate}
 \item  recovers in at most $k$ steps  (\emphcolor{bounded adaptation}),
\vspace{0.2cm}
 \item  eventually recovers  (\emphcolor{eventual adaptation}). 
\end{enumerate}
\end{block}
\end{frame}














\begin{frame}
 \frametitle{Example: Scaling in cloud computing}


\begin{itemize}
 \item An application in the cloud
$$
G  =  \componentbbig{g}{\, I \parallel \cdots \parallel I \parallel \emphcolor{S_{dw}} \parallel \emphcolor{S_{up}} \parallel \nmu{CTRL}_{i} \,}
$$

\vspace{0.5cm}

\item A way of controlling scaling
 $$
\begin{array}{l}
S_{dw}  =  \componentbbig{s_{d}}{\, !\,\nm{alert^{d}}.\prod^{j} \update{\nmu{mid}}{\nil}\, } \\
S_{up}  =  \componentbbig{s_{u}}{\, !\,\nm{alert^{u}}.\prod^{k} \updatebig{\nmu{mid}}{\component{\nmu{mid}}{\bullet} \parallel \component{\nmu{mid}}{\bullet}}\, }
 \end{array}
$$

\vspace{0.5cm}

\item A property to guarantee: every scaling alert  will disappear within a certain bound, i.e. the scaling request is promptly addressed by the cloud provider. 

\end{itemize}
\end{frame}



\begin{frame}
 \frametitle{Decidability of the verification problems}

\begin{itemize}
 \item Bounded and eventual adaptation are \emphcolor{undecidable} in \evol{}
\vspace{0.5cm}

 \item The verification problems can be related to \emphcolor{termination} in Turing Complete models
\vspace{0.5cm}
 \item If a Turing machine $M$ terminates then its encoding into \evol{} has
a computation where the error message is always available
 
\end{itemize}
\end{frame}

\begin{frame}
  \frametitle{The Minsky machine}
 
\begin{itemize}
 \item Numbers are represented as chains of prefixes: $u.u.u.z$ located inside an adaptable process
\vspace{0.5cm}
 \item The increment simply updates the adaptable process by prefixing with $u$ the old content
\vspace{0.5cm}
\item The decrement consumes one unit 
\end{itemize}


\end{frame}


\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& Dynamic Topology & Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
%\evol{2}	& ~ \OG dec~/~\LG undec ~ & ~ \OG dec~/~\LG undec \\
%\hline
%\evol{3}	& ~ \OG dec~/~\LG undec ~ & \OG~dec~/~\LG dec 
\end{tabular}
\end{center}

\end{frame}





\begin{frame}
 \frametitle{Towards decidability}

\begin{itemize}
 \item Are there any fragments where \OG or \LG can be decided?
\vspace{0.5cm}
 \item \emphcolor{Intuition}: to disallow some update patterns
%i.e. holes cannot appear behind prefixes
\vspace{0.5cm}
 \item Obtain fragments that are still powerful enough to model interesting scenarios 

\end{itemize}
\end{frame}


\begin{frame}
 \frametitle{First fragment: Unguarded \evol{}} 

\begin{itemize}
 \item Holes cannot appear behind prefixes
\end{itemize}

$$
U  ::=  P \, \mid \, \component{a}{U}  \, \mid \,    U \parallel U  \, \mid \, \bullet  
$$



\end{frame}


\begin{frame}
\frametitle{Some examples}
\begin{description}
\item[Replacement] $$\quad \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$$ 
\item[Destroyer]$$\quad \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (\bullet \not \in Q)$$
\item[Renaming] $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{\bullet}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item[Backup] $$\component{a}{Q} \parallel \update{a}{\component{a}{\bullet} \parallel \component{b}{\bullet}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\end{description}

\end{frame}




\begin{frame}
 \frametitle{Eventual Adaptation is undecidable}

\begin{itemize}
 \item \evol{2} is weakly Turing powerful
\vspace{0.5cm}

\item The encoding has 
an infinite sequence of  runs if and only 
if the corresponding \mm terminates. 

\vspace{0.5cm}
\item Termination can be related to the eventual adaptation problem

\end{itemize}

\end{frame}




\begin{frame}
\frametitle{Bounded adaptation is decidable in \evol{2}}

 \begin{center}
  The algorithm consists in checking whether it is  possible to \emphcolor{reach a
process greater} than one that exhibit at least $k$ signals
 \end{center}

This accounts in:
\begin{enumerate}
 \item  defining an ordering on states 
\vspace{0.2cm}
\item performing a symbolic backward analysis



\end{enumerate}
\begin{center}
\includegraphics[width=0.7\textwidth]{predanalisi.pdf} 
\end{center}
 
\end{frame}



\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& Dynamic Topology & Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
\evol{2}	& ~ \emphcolor{\OG dec}~/~\LG undec ~ & ~ \emphcolor{\OG dec}~/~\LG undec \\
\hline
%\evol{3}	& ~ \OG dec~/~\LG undec ~ & \OG~dec~/~\LG dec 
\end{tabular}
\end{center}

\end{frame}


\begin{frame}
\frametitle{The second fragment: Preserving \evol{}} 

\begin{itemize}
\item Current state of the adaptable process is always preserved.
\end{itemize}
$$
U  ::=  \component{a}{U}  \, \mid \,  U \parallel P \, \mid \, \bullet
$$


\end{frame}


\begin{frame}
\frametitle{Some examples}
\begin{description}
\item[Renaming] $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{\bullet}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item[Backup] $$\component{a}{Q} \parallel \update{a}{\component{a}{\bullet} \parallel \component{b}{\bullet}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\end{description}

\end{frame}




\begin{frame}
\frametitle{The dynamic calculus}

\begin{itemize}
 \item \evold{3} is still weakly Turing powerful

\vspace{0.5cm}

 \item Processes cannot be removed $\leadsto$ they are collected as garbage

\end{itemize}

 

\end{frame}


\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& Dynamic Topology & Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
\evol{2}	& ~ \OG dec~/~\LG undec ~ & ~ \OG dec~/~\LG undec \\
\hline
\evol{3}	& ~ \OG dec~/~\LG undec ~ & %\OG~dec~/~\LG dec 
\end{tabular}
\end{center}

\end{frame}

\begin{frame}
 \frametitle{The static calculus}

\begin{itemize}
 \item Eventual adaptation is decidable
 

\vspace{0.5cm}

\item \evols{3} can be encoded into Petri nets
\end{itemize}

 

\end{frame}



\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& Dynamic Topology & Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
\evol{2}	& ~ \OG dec~/~\LG undec ~ & ~ \OG dec~/~\LG undec \\
\hline
\evol{3}	& ~ \OG dec~/~\LG undec ~ & \OG~dec~/\emphcolor{~\LG dec} 
\end{tabular}
\end{center}

\end{frame}


\section{Conclusions}

\begin{frame}
 \frametitle{Summing up \dots}
 
\begin{itemize}
\item A process calculus approach to dynamic reconfiguration, evolvability, and adaptation
\vspace{0.2cm}
\item 
A basis for the development of more expressive languages, and for verification studies
\end{itemize}


\end{frame}

\begin{frame}
 \frametitle{Future works}

\begin{itemize}
 \item Dynamic reconfiguration in \evol{} with  priorities/fairness
\vspace{1cm}
 \item Type systems: safe updates and more refined abilities for the locations 

\end{itemize}


\end{frame}


\begin{frame}
 \frametitle{Further info}

\begin{itemize}
 \item Based on a work presented at FMOODS--FORTE 2011
\begin{block}{}
 \tiny
M. Bravetti, C. Di Giusto, J.A. P\`erez and G. Zavattaro.\\ Adaptable processes (Extended Abstract). FMOODS-FORTE 2011, LNCS, vol. 6722 pages 90--105
\end{block}
\vspace{1cm}

 \item Technical report available at 
\begin{center}
\emphcolor{\url{www.cs.unibo.it/~perez/ap/}}  
\end{center}
\end{itemize}


\end{frame}


\begin{frame}
 \frametitle{ Minsky machine for \evols{1}} 

\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_j \qquad
\encp{r_j = n}{\mmn{1}}   =  \component{r_j}{\encn{n}{j}} 
\)  \\%where
\quad where 
\quad  \(  
\encn{n}{j}=\left\{  
\begin{array}{ll}  
\overline{z_j}  & \textrm{if } n= 0 \\  
 \overline{u_j}.\encn{n-1}{j} & \textrm{if } n> 0 .  
\end{array}\right.  
\)
\\
\\
\\ 
\(
\begin{array}{ll}   
\multicolumn{2}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{1}} \!&= !p_i.\update{r_j}{\component{r_j}{\overline{u_j}.\bullet}}.\overline{p_{i+1}}\\
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{1}}\!&=  !p_i.(u_j.\overline{p_{i+1}} + z_j.\update{r_j}{\component{r_j}{\overline{z_j}}}.\overline{p_{s}})\\
\encp{(i: \mathtt{HALT})}{\mmn{1}}\!&=  !p_i.(e + %.\update{r_0}{\component{r_0}{\overline{z_0}}}.\update{r_1}{\component{r_1}{\overline{z_1}}}
\outC{p_i})
\end{array}   
\)
\end{tabular}

\end{frame}

\begin{frame}
 \frametitle{Minsky machine for \evols{2}}
 \begin{tabular}{l} 
$\controll ~= ~!a.(\outC{f} \parallel \outC{b} \parallel  \outC{a}) \parallel \outC{a}.a.(\outC{p_1} \parallel e) \parallel \
!h.(g.\outC{f} \parallel \outC{h})$
  \\
$\mathrm{\textsc{Register}}~r_j $ \\
\ \  \(  
\encp{r_j = m}{\mmn{2}}=\left\{  
\begin{array}{ll}  
 \component{r_j}{!inc_j.\outC{u_j} \parallel \outC{z_j}}  & \textrm{if } m= 0 \\  
 \component{r_j}{!inc_j.\outC{u_j} \parallel \prod^{m}\overline{u_j} \parallel \outC{z_j} }  
%\parallel \prod_{1}^{m}\overline{w} 
~~& \textrm{if } m> 0 .  
\end{array}\right.  
\) \\ 
\(   
\begin{array}{ll}   
\multicolumn{2}{l}{\mathrm{\textsc{\!\!Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{2}}&  =   !p_i.f.(\outC{g} \parallel b.\outC{inc_j}.
%(\outC{w} \parallel 
\outC{p_{i+1}})\\  
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{2}} \! \! \! \! \!&  =  !p_i.f.\big(\outC{g} \parallel (u_j.(\outC{b} \parallel
           \outC{p_{i+1}}) \\
& \qquad +   z_j.\update{r_j}{\component{r_j}{!inc_j.\outC{u_j} \parallel \outC{z_j}}}. \outC{p_s})\big) \\
\encp{(i: \mathtt{HALT})}{\mmn{2}}&  =  !p_i.%.w.
                  \outC{h}.h.\update{r_0}{\component{r_0}{!inc_0.\outC{u_0} \parallel \outC{z_0}}}.\\
& \qquad\update{r_1}{\component{r_1}{!inc_1.\outC{u_1} \parallel \outC{z_1}}}.\outC{p_1}
\end{array}   
\) 
\end{tabular}
\end{frame}

\begin{frame}
 \frametitle{Minsky machine for \evold{3}}
 {
\centering  
 
\begin{tabular}{l}   
$\controll ~= ~!a.(\outC{f} \parallel \outC{b} \parallel  \outC{a}) \parallel \outC{a}.a.(\outC{p_1} \parallel e) \parallel \
!h.(g.\outC{f} \parallel \outC{h})$
  \\
$\mathrm{\textsc{Register}}~r_j $ \\ 
\ \ \(  
\encp{r_j = 0 }{\mmn{3}}= \component{r_j}{Reg_j \parallel \component{c_j}{\nil}} 
\) \\
\ \ $\mbox{with~} Reg_j = !inc_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}.u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$
\\
\(
\begin{array}{lll}
\multicolumn{3}{l}{\! \! \mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{3}}&  = &  !p_i.f.(\outC{g} \parallel
b.\outC{inc_j}.
ack.\outC{p_{i+1}}) \\
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{3}}&  = & !p_i.f.\big(\outC{g} \parallel(\outC{u_j}.%(\outC{w}+
ack.(\outC{b} \parallel %w . 
\outC{p_{i+1}})  + \\%)
&&  \qquad \update{c_j}{\bullet}.\update{r_j}{\component{r_j}{Reg_j \parallel
\component{c_j}{\bullet}}}.\outC{p_s})\big) \\
\encp{(i: \mathtt{HALT})}{\mmn{3}}&  = & !p_i.%w.
\outC{h}.h.\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \\
&&  \qquad \update{c_1}{\bullet}.\update{r_1}{\component{r_1}{Reg_1 \parallel
\component{c_1}{\bullet}}}.\outC{p_1}
\end{array}   
\)
\end{tabular}
}

\end{frame}




\end{document}
